Nuprl Definition : cless
0,22
postcript
pdf
e
<
e'
==
e
,
e'
. pred!(
e
;
e'
)^+(
e
,
e'
)
latex
clarification:
cless(
E
;
pred?
;
info
;
e
;
e'
) == rel_plus(
E
; (
e
,
e'
. pred!(
E
;
pred?
;
info
;
e
;
e'
)))(
e
,
e'
)
latex
Definitions
pred!(
e
;
e'
)
,
R
^+
FDL editor aliases
cless
origin
e,e'. pred!(e;e')^+(e,e')
e,e'. pred!(E;pred?;info;e;e')))(e,e') e,e'. pred!(e;e')^+(e,e')
e,e'. pred!(E;pred?;info;e;e')))(e,e')